Nuprl Lemma : int-eq-in-rationals
11,40
postcript
pdf
x
,
y
:
. (
x
=
y
)
(
x
=
y
)
latex
Definitions
{
T
}
,
SQType(
T
)
,
tt
,
if
b
then
t
else
f
fi
,
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
qeq(
r
;
s
)
,
S
T
Lemmas
assert
of
eq
int
,
assert-qeq
,
int
inc
rationals
,
rationals
wf
origin
x, y:
. (x = y 
) 
(x = y) x, y:. (x = y ) (x = y) 
T Q Q Qx:A. B(x)
T